package ca.shojaei.mini_sat;
import java.util.Stack;
import java.util.regex.*;


/*		Some definitions

	    <expression>  ::=  [ "!" | "e@" | "a@" ] <factor> [["!"] [ "&" | "|" | "e@" | "a@" |
	    "eU" | "aU"] <factor> ]

	    <factor>  ::=  <char>  |  "(" <expression> ")"
 */


class OpAndSize{

	public Clause op;
	public int size;

	public OpAndSize(){}
}

class OpAndString{

	public Clause op;
	public String left;
	public String right;

	public OpAndString(){}
}


public class Parser {
	static class ParseError extends Exception {
		// Represents a syntax error found in the user's input.
		ParseError(String message) {
			super(message);
		}
	} // end nested class ParseError

	static OpAndString FindMainOperator(String inputString){
		OpAndString os = new OpAndString();
		String input = inputString;
		int i = 0;//MAKE SURE WE DON'T PASS AN INITIAL '('

		boolean negation;  // True if there is a leading minus sign.
		negation = false;
		if (input.charAt(i) == '!') {
			negation = true;
			String str = input.substring(1);
			String strCleaned = cleanString(str);
			input = strCleaned;
		}		
		OpAndSize clause;
		//Determine if the main operator is unary
		int operator = isOperator(input.charAt(i), input.charAt(i +1));
		if(operator == 1 || operator == 2){
			clause = getOperator(input.charAt(i), input.charAt(i+1));
			clause.op.setNegated(negation);
			os.op = clause.op;
			os.left = cleanString(input.substring(i+ clause.size));
			os.right = "";
		}
		//The following is for a binary operator
		else{
			boolean done = false;
			int leftB = -1;
			while(!done){	
				if(input.charAt(i) == '('){
					if(leftB == -1)
						leftB = 1;
					else 
						leftB ++;
				}
				else 
					if(input.charAt(i) == ')')
						leftB --;
				
				if(leftB == 0){
					done = true;
					break;
				}
				else
					i++;
			}
			if(done){
				String substring = input.substring(0, i + 1);
				os.left = cleanString(substring);
			}

			clause = getOperator(input.charAt(i + 1), input.charAt(i+2));
			clause.op.setNegated(negation);
			os.op = clause.op;
			os.right = cleanString(input.substring(i + 1 + clause.size));
		}
		return os;
	}

	static Clause Parse(String inputString) throws ParseError{
		
		String input = removeBlanks(inputString);
		Clause clause;
		if(!StringHasOperator(input)){
			clause = noOperator(input);
		}
		else{

			OpAndString ops = FindMainOperator(input);
			
			clause = ops.op;
			Clause left = parseString(ops.left, 0,clause,false);
			clause.setLeft(left);
			if(!ops.right.equals("")){
				Clause right = parseString(ops.right, 0,clause,true);
				clause.setRight(right);
			}
		}
		return clause;
	}
	
	static Clause noOperator(String inputString){
			
		int i = 0;
		boolean negation;  // True if there is a leading ! sign.
		negation = false;
		if (inputString.charAt(i) == '!') {
			negation = true;
			i++;
		}
		Clause clause = new Item(String.valueOf(inputString.charAt(i)));
		clause.setNegated(negation);
		return clause;
	}
	
	static boolean StringHasOperator(String inputString){

		if(inputString.contains("&") || inputString.contains("|") || inputString.contains("e@") ||
				inputString.contains("a@") || inputString.contains("eU") || inputString.contains("aU")){
			return true;
		}
		else{
			return false;
		}
	}

	static Clause parseString(String inputString, int pos, Clause clause, boolean right) throws ParseError{

		/*<expression>  =  [ "!" | "e@" | "a@" ] <factor> [ [ "&" | "|" | "e@" | "a@" |
		"eU" | "aU" | "!" ] <factor> ]
	   <factor>  =  <char>  |  "(" <expression> ")"                                            	    
		 */
		//TODO: Pass to the function the first position after the first parenthesis!
		Clause child;
		if(!StringHasOperator(inputString)){
			boolean negation;  // True if there is a leading ! sign.
			negation = false;
			if (inputString.charAt(pos) == '!') {
				negation = true;
				pos++;
			}
			child = new Item(String.valueOf(inputString.charAt(pos)));
			child.setNegated(negation);

			if(right)
				clause.setRight(child);
			else
				clause.setLeft(child);
		}
		else{
			OpAndString ops = FindMainOperator(inputString);
			child = ops.op;

			Clause left = parseString(ops.left, 0,child,false);
			Clause rightC = null;
			if(!ops.right.equals(""))
				rightC = parseString(ops.right, 0,child,true);

			child.setLeft(left);
			child.setRight(rightC);

			if(right)
				clause.setRight(child);
			else
				clause.setLeft(child);
		}
		return child;
	}

	static boolean notSpecial(char c){
		if(c != '!' || c != '&' || c!= '(' || c!= ')')
			return true;
		else
			return false;
	}

	static String removeBlanks(String input){

		String str = input;
		int index = str.lastIndexOf(' ');
		
		while(index >= 0 ){
			
			str = str.substring(0, index).concat(str.substring(index+1));
			index = str.lastIndexOf(' ');
		}
		return str;
	}

	static String cleanString(String input){
		
		if((input.charAt(0) == '(') && (input.charAt(input.length() - 1) == ')'))
				return input.substring(1,input.length() - 1);
		return input;
	}
	
	static int isOperator(char a, char b){

		if((a == '&') || (a == '|'))
			return 1;
		else if((a == 'e' || a == 'a') && (b == '@' || b == 'U'))
			return 2;
		else 
			return 0;
	}

	static OpAndSize getOperator(char a, char b){

		
		char[] op = null;
		if((a == '&') || (a == '|')){
			op = new char[1];
			op[0] = a;
		}
		else if((a == 'e' || a == 'a') && (b == '@' || b == 'U')){
			op = new char[2];
			op[0] = a;
			op[1] = b;
		}
		
		String str = String.copyValueOf(op);
		return getOperatorAndSizeClass(str);
	}

	static OpAndSize getOperatorAndSizeClass(String op){

		OpAndSize opS = new OpAndSize();
		opS.op = null;
		opS.size = 1;
		if(op.equals("&"))
			opS.op = new And();
		else{
			if(op.equals("|")){
				opS.op = new Or();
			}
			else{
				opS.size = 2;
				if(op.equals("eU")){
					opS.op = new ExistsUntil();
				}
				if(op.equals("e@")){
					opS.op = new ExistsNext();
				}
				if(op.equals("aU")){
					opS.op = new ForAllUntil();
				}
				if(op.equals("a@"))
					opS.op = new ForAllNext();
			}

		}

		return opS;
	}

	static String getClassOperator(String op){

		if(op.equals("&"))
			return "And";
		if(op.equals("|"))
			return "Or";
		if(op.equals("eU"))
			return "ExistsUntil";
		if(op.equals("e@"))
			return "ExistsNext";
		if(op.equals("aU"))
			return "ForAllUntil";
		if(op.equals("a@"))
			return "ForAllNext";    		
		else
			return " ";
	}

	static Clause getClass(String op){

		if(op.equals("&"))
			return new And();
		if(op.equals("|"))
			return new Or();
		if(op.equals("eU"))
			return new ExistsUntil();
		if(op.equals("e@"))
			return new ExistsNext();
		if(op.equals("aU"))
			return new ForAllUntil();
		if(op.equals("a@"))
			return new ForAllNext();    		
		else
			return null;
	}
	
	static void printClause(Clause clause){
		
		System.out.print("( ");
		if(clause.getLeft() != null) 
			printClause(clause.getLeft());	
		System.out.print(clause.getSymbol());
		if(clause.getRight() != null) 
			printClause(clause.getRight());	
		System.out.print(" )");
	}
	
	static void printTreeClause(Clause clause){

		System.out.println("PARENT OR LEAVE: " + clause.getSymbol());
		if(clause.getLeft() != null)
			System.out.print("Left Child: " + clause.getLeft().getSymbol() + " ");
		if(clause.getRight() != null)
			System.out.print("Right Child: " + clause.getRight().getSymbol() + " " + "\n");
		else 
			System.out.print("\n");
		if(clause.getLeft() != null)
			printTreeClause(clause.getLeft());
		if(clause.getRight() != null)
			printTreeClause(clause.getRight());
	}
	
	
	
	/* TODO:Error handling
 static boolean rightFormat(String input){

	 for()
	 return false;

 }*/
}//End of Parser Class



